k:Knd, l:IdLnk, dt:x:Id fp Type. k  dom(lnk-decl(l;dt))  {isrcv(k) & tag(k)  dom(dt)} 

latex

Definitions	b, tag(k), isrcv(k), x:AB(x), left+right, Knd, t  T, IdLnk, Id, Type, x. t(x), x:A. B(x), a:A fp B(a), lnk-decl(l;dt), x.A(x), Top, x:AB(x), KindDeq, x  dom(f), {T}, P  Q, True, A & B, SQType(T), s = t, Prop, s ~ t, False
Lemmas	lnk-decl-dom-not, lnk-decl-dom2, IdLnk sq, lnk-decl-dom, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, Id wf, IdLnk wf, Knd wf